Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
c(0,x) |
→ x |
| 2: |
|
c(x,c(y,z)) |
→ c(x + y,z) |
| 3: |
|
0 + 0 |
→ 0 |
| 4: |
|
0 + 1 |
→ 1 |
| 5: |
|
0 + 2 |
→ 2 |
| 6: |
|
0 + 3 |
→ 3 |
| 7: |
|
0 + 4 |
→ 4 |
| 8: |
|
0 + 5 |
→ 5 |
| 9: |
|
0 + 6 |
→ 6 |
| 10: |
|
0 + 7 |
→ 7 |
| 11: |
|
0 + 8 |
→ 8 |
| 12: |
|
0 + 9 |
→ 9 |
| 13: |
|
1 + 0 |
→ 1 |
| 14: |
|
1 + 1 |
→ 2 |
| 15: |
|
1 + 2 |
→ 3 |
| 16: |
|
1 + 3 |
→ 4 |
| 17: |
|
1 + 4 |
→ 5 |
| 18: |
|
1 + 5 |
→ 6 |
| 19: |
|
1 + 6 |
→ 7 |
| 20: |
|
1 + 7 |
→ 8 |
| 21: |
|
1 + 8 |
→ 9 |
| 22: |
|
1 + 9 |
→ c(1,0) |
| 23: |
|
2 + 0 |
→ 2 |
| 24: |
|
2 + 1 |
→ 3 |
| 25: |
|
2 + 2 |
→ 4 |
| 26: |
|
2 + 3 |
→ 5 |
| 27: |
|
2 + 4 |
→ 6 |
| 28: |
|
2 + 5 |
→ 7 |
| 29: |
|
2 + 6 |
→ 8 |
| 30: |
|
2 + 7 |
→ 9 |
| 31: |
|
2 + 8 |
→ c(1,0) |
| 32: |
|
2 + 9 |
→ c(1,1) |
| 33: |
|
3 + 0 |
→ 3 |
| 34: |
|
3 + 1 |
→ 4 |
| 35: |
|
3 + 2 |
→ 5 |
| 36: |
|
3 + 3 |
→ 6 |
| 37: |
|
3 + 4 |
→ 7 |
| 38: |
|
3 + 5 |
→ 8 |
| 39: |
|
3 + 6 |
→ 9 |
| 40: |
|
3 + 7 |
→ c(1,0) |
| 41: |
|
3 + 8 |
→ c(1,1) |
| 42: |
|
3 + 9 |
→ c(1,2) |
| 43: |
|
4 + 0 |
→ 4 |
| 44: |
|
4 + 1 |
→ 5 |
| 45: |
|
4 + 2 |
→ 6 |
| 46: |
|
4 + 3 |
→ 7 |
| 47: |
|
4 + 4 |
→ 8 |
| 48: |
|
4 + 5 |
→ 9 |
| 49: |
|
4 + 6 |
→ c(1,0) |
| 50: |
|
4 + 7 |
→ c(1,1) |
| 51: |
|
4 + 8 |
→ c(1,2) |
| 52: |
|
4 + 9 |
→ c(1,3) |
| 53: |
|
5 + 0 |
→ 5 |
| 54: |
|
5 + 1 |
→ 6 |
| 55: |
|
5 + 2 |
→ 7 |
| 56: |
|
5 + 3 |
→ 8 |
| 57: |
|
5 + 4 |
→ 9 |
| 58: |
|
5 + 5 |
→ c(1,0) |
| 59: |
|
5 + 6 |
→ c(1,1) |
| 60: |
|
5 + 7 |
→ c(1,2) |
| 61: |
|
5 + 8 |
→ c(1,3) |
| 62: |
|
5 + 9 |
→ c(1,4) |
| 63: |
|
6 + 0 |
→ 6 |
| 64: |
|
6 + 1 |
→ 7 |
| 65: |
|
6 + 2 |
→ 8 |
| 66: |
|
6 + 3 |
→ 9 |
| 67: |
|
6 + 4 |
→ c(1,0) |
| 68: |
|
6 + 5 |
→ c(1,1) |
| 69: |
|
6 + 6 |
→ c(1,2) |
| 70: |
|
6 + 7 |
→ c(1,3) |
| 71: |
|
6 + 8 |
→ c(1,4) |
| 72: |
|
6 + 9 |
→ c(1,5) |
| 73: |
|
7 + 0 |
→ 7 |
| 74: |
|
7 + 1 |
→ 8 |
| 75: |
|
7 + 2 |
→ 9 |
| 76: |
|
7 + 3 |
→ c(1,0) |
| 77: |
|
7 + 4 |
→ c(1,1) |
| 78: |
|
7 + 5 |
→ c(1,2) |
| 79: |
|
7 + 6 |
→ c(1,3) |
| 80: |
|
7 + 7 |
→ c(1,4) |
| 81: |
|
7 + 8 |
→ c(1,5) |
| 82: |
|
7 + 9 |
→ c(1,6) |
| 83: |
|
8 + 0 |
→ 8 |
| 84: |
|
8 + 1 |
→ 9 |
| 85: |
|
8 + 2 |
→ c(1,0) |
| 86: |
|
8 + 3 |
→ c(1,1) |
| 87: |
|
8 + 4 |
→ c(1,2) |
| 88: |
|
8 + 5 |
→ c(1,3) |
| 89: |
|
8 + 6 |
→ c(1,4) |
| 90: |
|
8 + 7 |
→ c(1,5) |
| 91: |
|
8 + 8 |
→ c(1,6) |
| 92: |
|
8 + 9 |
→ c(1,7) |
| 93: |
|
9 + 0 |
→ 9 |
| 94: |
|
9 + 1 |
→ c(1,0) |
| 95: |
|
9 + 2 |
→ c(1,1) |
| 96: |
|
9 + 3 |
→ c(1,2) |
| 97: |
|
9 + 4 |
→ c(1,3) |
| 98: |
|
9 + 5 |
→ c(1,4) |
| 99: |
|
9 + 6 |
→ c(1,5) |
| 100: |
|
9 + 7 |
→ c(1,6) |
| 101: |
|
9 + 8 |
→ c(1,7) |
| 102: |
|
9 + 9 |
→ c(1,8) |
| 103: |
|
x + c(y,z) |
→ c(y,x + z) |
| 104: |
|
c(x,y) + z |
→ c(x,y + z) |
| 105: |
|
0 * 0 |
→ 0 |
| 106: |
|
0 * 1 |
→ 0 |
| 107: |
|
0 * 2 |
→ 0 |
| 108: |
|
0 * 3 |
→ 0 |
| 109: |
|
0 * 4 |
→ 0 |
| 110: |
|
0 * 5 |
→ 0 |
| 111: |
|
0 * 6 |
→ 0 |
| 112: |
|
0 * 7 |
→ 0 |
| 113: |
|
0 * 8 |
→ 0 |
| 114: |
|
0 * 9 |
→ 0 |
| 115: |
|
1 * 0 |
→ 0 |
| 116: |
|
1 * 1 |
→ 1 |
| 117: |
|
1 * 2 |
→ 2 |
| 118: |
|
1 * 3 |
→ 3 |
| 119: |
|
1 * 4 |
→ 4 |
| 120: |
|
1 * 5 |
→ 5 |
| 121: |
|
1 * 6 |
→ 6 |
| 122: |
|
1 * 7 |
→ 7 |
| 123: |
|
1 * 8 |
→ 8 |
| 124: |
|
1 * 9 |
→ 9 |
| 125: |
|
2 * 0 |
→ 0 |
| 126: |
|
2 * 1 |
→ 2 |
| 127: |
|
2 * 2 |
→ 4 |
| 128: |
|
2 * 3 |
→ 6 |
| 129: |
|
2 * 4 |
→ 8 |
| 130: |
|
2 * 5 |
→ c(1,0) |
| 131: |
|
2 * 6 |
→ c(1,2) |
| 132: |
|
2 * 7 |
→ c(1,4) |
| 133: |
|
2 * 8 |
→ c(1,6) |
| 134: |
|
2 * 9 |
→ c(1,8) |
| 135: |
|
3 * 0 |
→ 0 |
| 136: |
|
3 * 1 |
→ 3 |
| 137: |
|
3 * 2 |
→ 6 |
| 138: |
|
3 * 3 |
→ 9 |
| 139: |
|
3 * 4 |
→ c(1,2) |
| 140: |
|
3 * 5 |
→ c(1,5) |
| 141: |
|
3 * 6 |
→ c(1,8) |
| 142: |
|
3 * 7 |
→ c(2,1) |
| 143: |
|
3 * 8 |
→ c(2,4) |
| 144: |
|
3 * 9 |
→ c(2,7) |
| 145: |
|
4 * 0 |
→ 0 |
| 146: |
|
4 * 1 |
→ 4 |
| 147: |
|
4 * 2 |
→ 8 |
| 148: |
|
4 * 3 |
→ c(1,2) |
| 149: |
|
4 * 4 |
→ c(1,6) |
| 150: |
|
4 * 5 |
→ c(2,0) |
| 151: |
|
4 * 6 |
→ c(2,4) |
| 152: |
|
4 * 7 |
→ c(2,8) |
| 153: |
|
4 * 8 |
→ c(3,2) |
| 154: |
|
4 * 9 |
→ c(3,6) |
| 155: |
|
5 * 0 |
→ 0 |
| 156: |
|
5 * 1 |
→ 5 |
| 157: |
|
5 * 2 |
→ c(1,0) |
| 158: |
|
5 * 3 |
→ c(1,5) |
| 159: |
|
5 * 4 |
→ c(2,0) |
| 160: |
|
5 * 5 |
→ c(2,5) |
| 161: |
|
5 * 6 |
→ c(3,0) |
| 162: |
|
5 * 7 |
→ c(3,5) |
| 163: |
|
5 * 8 |
→ c(4,0) |
| 164: |
|
5 * 9 |
→ c(4,5) |
| 165: |
|
6 * 0 |
→ 0 |
| 166: |
|
6 * 1 |
→ 6 |
| 167: |
|
6 * 2 |
→ c(1,2) |
| 168: |
|
6 * 3 |
→ c(1,8) |
| 169: |
|
6 * 4 |
→ c(2,4) |
| 170: |
|
6 * 5 |
→ c(3,0) |
| 171: |
|
6 * 6 |
→ c(3,6) |
| 172: |
|
6 * 7 |
→ c(4,2) |
| 173: |
|
6 * 8 |
→ c(4,8) |
| 174: |
|
6 * 9 |
→ c(5,4) |
| 175: |
|
7 * 0 |
→ 0 |
| 176: |
|
7 * 1 |
→ 7 |
| 177: |
|
7 * 2 |
→ c(1,4) |
| 178: |
|
7 * 3 |
→ c(2,1) |
| 179: |
|
7 * 4 |
→ c(2,8) |
| 180: |
|
7 * 5 |
→ c(3,5) |
| 181: |
|
7 * 6 |
→ c(4,2) |
| 182: |
|
7 * 7 |
→ c(4,9) |
| 183: |
|
7 * 8 |
→ c(5,6) |
| 184: |
|
7 * 9 |
→ c(6,3) |
| 185: |
|
8 * 0 |
→ 0 |
| 186: |
|
8 * 1 |
→ 8 |
| 187: |
|
8 * 2 |
→ c(1,8) |
| 188: |
|
8 * 3 |
→ c(2,4) |
| 189: |
|
8 * 4 |
→ c(3,2) |
| 190: |
|
8 * 5 |
→ c(4,0) |
| 191: |
|
8 * 6 |
→ c(4,8) |
| 192: |
|
8 * 7 |
→ c(5,6) |
| 193: |
|
8 * 8 |
→ c(6,4) |
| 194: |
|
8 * 9 |
→ c(7,2) |
| 195: |
|
9 * 0 |
→ 0 |
| 196: |
|
9 * 1 |
→ 9 |
| 197: |
|
9 * 2 |
→ c(1,8) |
| 198: |
|
9 * 3 |
→ c(2,7) |
| 199: |
|
9 * 4 |
→ c(3,6) |
| 200: |
|
9 * 5 |
→ c(4,5) |
| 201: |
|
9 * 6 |
→ c(5,4) |
| 202: |
|
9 * 7 |
→ c(6,3) |
| 203: |
|
9 * 8 |
→ c(7,2) |
| 204: |
|
9 * 9 |
→ c(8,1) |
| 205: |
|
x * c(y,z) |
→ c(x * y,x * z) |
| 206: |
|
c(x,y) * z |
→ c(x * z,y * z) |
|
There are 115 dependency pairs:
|
| 207: |
|
C(x,c(y,z)) |
→ C(x + y,z) |
| 208: |
|
C(x,c(y,z)) |
→ x +# y |
| 209: |
|
1 +# 9 |
→ C(1,0) |
| 210: |
|
2 +# 8 |
→ C(1,0) |
| 211: |
|
2 +# 9 |
→ C(1,1) |
| 212: |
|
3 +# 7 |
→ C(1,0) |
| 213: |
|
3 +# 8 |
→ C(1,1) |
| 214: |
|
3 +# 9 |
→ C(1,2) |
| 215: |
|
4 +# 6 |
→ C(1,0) |
| 216: |
|
4 +# 7 |
→ C(1,1) |
| 217: |
|
4 +# 8 |
→ C(1,2) |
| 218: |
|
4 +# 9 |
→ C(1,3) |
| 219: |
|
5 +# 5 |
→ C(1,0) |
| 220: |
|
5 +# 6 |
→ C(1,1) |
| 221: |
|
5 +# 7 |
→ C(1,2) |
| 222: |
|
5 +# 8 |
→ C(1,3) |
| 223: |
|
5 +# 9 |
→ C(1,4) |
| 224: |
|
6 +# 4 |
→ C(1,0) |
| 225: |
|
6 +# 5 |
→ C(1,1) |
| 226: |
|
6 +# 6 |
→ C(1,2) |
| 227: |
|
6 +# 7 |
→ C(1,3) |
| 228: |
|
6 +# 8 |
→ C(1,4) |
| 229: |
|
6 +# 9 |
→ C(1,5) |
| 230: |
|
7 +# 3 |
→ C(1,0) |
| 231: |
|
7 +# 4 |
→ C(1,1) |
| 232: |
|
7 +# 5 |
→ C(1,2) |
| 233: |
|
7 +# 6 |
→ C(1,3) |
| 234: |
|
7 +# 7 |
→ C(1,4) |
| 235: |
|
7 +# 8 |
→ C(1,5) |
| 236: |
|
7 +# 9 |
→ C(1,6) |
| 237: |
|
8 +# 2 |
→ C(1,0) |
| 238: |
|
8 +# 3 |
→ C(1,1) |
| 239: |
|
8 +# 4 |
→ C(1,2) |
| 240: |
|
8 +# 5 |
→ C(1,3) |
| 241: |
|
8 +# 6 |
→ C(1,4) |
| 242: |
|
8 +# 7 |
→ C(1,5) |
| 243: |
|
8 +# 8 |
→ C(1,6) |
| 244: |
|
8 +# 9 |
→ C(1,7) |
| 245: |
|
9 +# 1 |
→ C(1,0) |
| 246: |
|
9 +# 2 |
→ C(1,1) |
| 247: |
|
9 +# 3 |
→ C(1,2) |
| 248: |
|
9 +# 4 |
→ C(1,3) |
| 249: |
|
9 +# 5 |
→ C(1,4) |
| 250: |
|
9 +# 6 |
→ C(1,5) |
| 251: |
|
9 +# 7 |
→ C(1,6) |
| 252: |
|
9 +# 8 |
→ C(1,7) |
| 253: |
|
9 +# 9 |
→ C(1,8) |
| 254: |
|
x +# c(y,z) |
→ C(y,x + z) |
| 255: |
|
x +# c(y,z) |
→ x +# z |
| 256: |
|
c(x,y) +# z |
→ C(x,y + z) |
| 257: |
|
c(x,y) +# z |
→ y +# z |
| 258: |
|
2 *# 5 |
→ C(1,0) |
| 259: |
|
2 *# 6 |
→ C(1,2) |
| 260: |
|
2 *# 7 |
→ C(1,4) |
| 261: |
|
2 *# 8 |
→ C(1,6) |
| 262: |
|
2 *# 9 |
→ C(1,8) |
| 263: |
|
3 *# 4 |
→ C(1,2) |
| 264: |
|
3 *# 5 |
→ C(1,5) |
| 265: |
|
3 *# 6 |
→ C(1,8) |
| 266: |
|
3 *# 7 |
→ C(2,1) |
| 267: |
|
3 *# 8 |
→ C(2,4) |
| 268: |
|
3 *# 9 |
→ C(2,7) |
| 269: |
|
4 *# 3 |
→ C(1,2) |
| 270: |
|
4 *# 4 |
→ C(1,6) |
| 271: |
|
4 *# 5 |
→ C(2,0) |
| 272: |
|
4 *# 6 |
→ C(2,4) |
| 273: |
|
4 *# 7 |
→ C(2,8) |
| 274: |
|
4 *# 8 |
→ C(3,2) |
| 275: |
|
4 *# 9 |
→ C(3,6) |
| 276: |
|
5 *# 2 |
→ C(1,0) |
| 277: |
|
5 *# 3 |
→ C(1,5) |
| 278: |
|
5 *# 4 |
→ C(2,0) |
| 279: |
|
5 *# 5 |
→ C(2,5) |
| 280: |
|
5 *# 6 |
→ C(3,0) |
| 281: |
|
5 *# 7 |
→ C(3,5) |
| 282: |
|
5 *# 8 |
→ C(4,0) |
| 283: |
|
5 *# 9 |
→ C(4,5) |
| 284: |
|
6 *# 2 |
→ C(1,2) |
| 285: |
|
6 *# 3 |
→ C(1,8) |
| 286: |
|
6 *# 4 |
→ C(2,4) |
| 287: |
|
6 *# 5 |
→ C(3,0) |
| 288: |
|
6 *# 6 |
→ C(3,6) |
| 289: |
|
6 *# 7 |
→ C(4,2) |
| 290: |
|
6 *# 8 |
→ C(4,8) |
| 291: |
|
6 *# 9 |
→ C(5,4) |
| 292: |
|
7 *# 2 |
→ C(1,4) |
| 293: |
|
7 *# 3 |
→ C(2,1) |
| 294: |
|
7 *# 4 |
→ C(2,8) |
| 295: |
|
7 *# 5 |
→ C(3,5) |
| 296: |
|
7 *# 6 |
→ C(4,2) |
| 297: |
|
7 *# 7 |
→ C(4,9) |
| 298: |
|
7 *# 8 |
→ C(5,6) |
| 299: |
|
7 *# 9 |
→ C(6,3) |
| 300: |
|
8 *# 2 |
→ C(1,8) |
| 301: |
|
8 *# 3 |
→ C(2,4) |
| 302: |
|
8 *# 4 |
→ C(3,2) |
| 303: |
|
8 *# 5 |
→ C(4,0) |
| 304: |
|
8 *# 6 |
→ C(4,8) |
| 305: |
|
8 *# 7 |
→ C(5,6) |
| 306: |
|
8 *# 8 |
→ C(6,4) |
| 307: |
|
8 *# 9 |
→ C(7,2) |
| 308: |
|
9 *# 2 |
→ C(1,8) |
| 309: |
|
9 *# 3 |
→ C(2,7) |
| 310: |
|
9 *# 4 |
→ C(3,6) |
| 311: |
|
9 *# 5 |
→ C(4,5) |
| 312: |
|
9 *# 6 |
→ C(5,4) |
| 313: |
|
9 *# 7 |
→ C(6,3) |
| 314: |
|
9 *# 8 |
→ C(7,2) |
| 315: |
|
9 *# 9 |
→ C(8,1) |
| 316: |
|
x *# c(y,z) |
→ C(x * y,x * z) |
| 317: |
|
x *# c(y,z) |
→ x *# y |
| 318: |
|
x *# c(y,z) |
→ x *# z |
| 319: |
|
c(x,y) *# z |
→ C(x * z,y * z) |
| 320: |
|
c(x,y) *# z |
→ x *# z |
| 321: |
|
c(x,y) *# z |
→ y *# z |
|
The approximated dependency graph contains 2 SCCs:
{207,208,254-257}
and {317,318,320,321}.
-
Consider the SCC {207,208,254-257}.
The usable rules are {1-104}.
The constraints could not be solved.
-
Consider the SCC {317,318,320,321}.
There are no usable rules.
By taking the AF π with
π(*#) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {317,318}
are weakly decreasing and
the rules in {320,321}
are strictly decreasing.
There is one new SCC.
-
Consider the SCC {317,318}.
By taking the AF π with
π(*#) = 2 together with
the lexicographic path order with
empty precedence,
the rules in {317,318}
are strictly decreasing.
Tyrolean Termination Tool (39.58 seconds)
--- May 4, 2006